#import "@preview/frame-it:1.1.2": *
#import "RoseL_Snippets.typ": *
#show: RoseLic


语言是可以用来认知、交流、行事的.
其中数学 (mathema·tics) 作为规矩的学问,
包含对语言的一部分统一处理范式.
在辩论中, 自然语言被无死角地回顾,
从而塑造出了精确的数学语言.

亚里士多德给出了从自然语言中塑造命题的规则.
而在数学语言中, 数理逻辑负责从已有命题产生新的命题, 
创造命题的任务则交给其他数学分支.
事实上这正是数学的精髓之一, 把书读薄,
把大量结论串接在尽可能少的原始命题上, 汇聚成知识网络.

== 蕴含和否定

用简单句构筑复杂句的一种方法是使用关联词,
比如 "并不是..." 和 "只要...就..." 等.

数学语言中使用可以带角标的单个字母表示命题, 
比如 $p$ 或者 $T$. 
// 源自proposition(english)和ti(chinese)
本书中使用 $T_(n (m))$ 的记号表示 
"习题 $n$ 的第 $(m)$ 项命题".

#notation[否定 $not$ (negation)][
  // 被否定项 (negated component)][
  #term[否定]是关于一个#forward[命题]的#forward[谓词], 
  通常说成 "并非#term[被否定项]", 
  记作 $ not P_c $
]
// 比较入机的叫法是: 项的否定
// 如果被否定项是关系表达式, 
// 那么还可以直接在关系符上打一斜线

#notation[蕴含 $->$ (conditional)][
  // 前件 (antecedent)][后件 (consequence)][
  #term[蕴含]是关于两个#forward[命题]的#forward[谓词], 
  通常说成 "如果#term[前件], 那么#term[后件]", 
  记作 $ P_a -> P_c $
]
// 比较入机的叫法是: 前件与后件的蕴含

// 从现在开始讨论蕴含和否定的算律. 
蕴含的运算优先级低于否定. 

作为一种具有公理化风格的写法, 
本文希望下列4条基本规则足以描述蕴含式和否定式的概念. 

#axiom[前提引入][
  $ p -> (q -> p) $
]<前提引入>

给命题 $p$ 引入前提 $q$, 得到蕴含式 $q->p$.

一个命题成立了, 就可以给这个命题加一个前提条件. 
"前提条件" 也是术语 "前件" 的来源.

#axiom[前提分配][
  $ (r->(q->p)) -> ((r->q)->(r->p)) $
  // $ ((c->b)->(c->a)) -> (c->(b->a)) $
]<前提分配>

给蕴含式 $q->p$ 整体引入前提 $r$,
相当于给它的前件 $q$ 和后件 $p$ 分别引入前提 $r$, 
再连成的蕴含式.
// 反之, 如果一个蕴含式的前件和后件都是蕴含式,
// 而且它们有共同的前件, 那么这个共同的前件可以提取出来. 后面会讲

#axiom[否定引入][
 $ (q -> p) -> (not p -> not q) $
]<否定引入>

#axiom[否定消除][
  $ not (not p) -> p $
]<否定消除>
这是经典的逆否命题和双重否定. 
由此我们可以明确命题的概念. 

#definition[命题 (proposition)][
  #term[命题]是陈述性的语句, 可以代入到@前提引入 \~ @否定消除
  中使它们始终成立.
]

自圆其说就是真, 反之, 真就可以用重言式 (tautology) 来定义.

#definition[真值 (truth)][
  #term[真]就是#forward[每一个]@命题\对自身的@蕴含.
  $ top := (p->p) quad #forward[$(forall p)$] $
  #divide()
  #term[假]就是@真\的@否定.
  $ bot := not top $
]

非真即假. 真和假是不同的命题常量.
// @否定消除 保证命题常量只有两个. 后面会讲

蕴含关系本身可以构成推理, 
它的字面表达就对应着如下的推理形式, 
即蕴含式成立时, 借助前件成立, 推出后件成立. 
若不成立, 则不可以使用这个推理形式.
// 作为真值推演, 它只有两个前提为真时, 结论才为真. 
#algorithm[假言推理 (modus ponens)][$
  (quad p->q quad\ p)/q
$]<假言推理>
#algorithm[假言三段论 \ (hypothetical syllogism)][$
  (quad p->q quad \ q->r)/(p->r)                    
$]<假言三段论>
#algorithm[两难推理 (dilemma)][$
  (quad p & -> q quad \ not p & -> q)/q                 
$]<两难推理>

// 一个定理要从公式和算法两个方向考虑. 
// 取拒式我是想开除算法籍的, 太没用(?) 
// 本文的所有链接都是为证明模块服务的,
// 当然定义和定理等模块也使用, 但正文就不使用了.
// 如果一个定理反复使用, 那么只在第一次时给链接. 
// 但如果涉及什么正用逆用斜着用, 
// 还又拉出它的公式大加改造, 那么每个不同用法给链接.

以下推论将所引入的公理补齐成为较为完整的对称形式. 
它们的证明普遍需要使用假言推理和假言三段论.

#exercise[][空证明][$
  not a -> (a -> b) 
$]<空证明>
基于 $p$ 为假的事实而对蕴含式 $p->q$ 
的证明称作空证明, 而基于 $q$ 为真的事实而对蕴含式
$p->q$ 的证明称作平凡证明. 

#corollary[@前提分配 \~ @否定消除 的逆命题][
$ a -> not (not a) $
#divide()
$ (not a -> not b) -> (b -> a) $
#divide()
$ ((c->b)->(c->a)) -> (c->(b->a)) $ 
]<双重否定引入>
#proof[][
  向否定消除式 (@否定消除) 中引入否定 (@否定引入) 得到
  $ not p -> not (not (not p)) $
  代入 $not p = a$ 得到
  $ a -> not (not a) $
  即为所证, 可知双重否定的#forward[等价]性. 
  // 那么该推论叫做双重否定引入. 
  #h(1fr) $qed$
  #divide()
  向否定引入式 (@否定引入) 中代入 $p = not a, q = not b$ 得到 
  $ (not b -> not a) -> (not (not a) -> not (not b)) $
  从而对该式@后件\的@前件\和@后件\同时消除双重否定
  (@否定消除), 得到 (为什么?)
  $ (not b -> not a) -> (a -> b) $
  即为所证, 可知逆否命题的#forward[等价]性. 
  // 那么该推论叫做逆转否定消除. 
  #h(1fr) $qed$
  #divide()
  设 $c$ 为真, 有假言推理 (@假言推理)
  $ (c -> a) -> a $
  (为什么?) 再由前提引入 (@前提引入) 即 
  $ b -> (c -> b) $
  进而基于假言三段论, 成立
  $ ((c -> b) -> (c -> a)) -> (b -> a) $
  再给它的后件引入前提, 依假言三段论得到要证式子; 

  设 $c$ 为假, 则要证式子是平凡的;

  总之, 这个两难推理使得式
  $ ((c->b)->(c->a)) -> (c->(b->a)) $ 
  总是成立, 可知前提分配的#forward[等价]性. 
  #h(1fr) $qed$
]

在上述证明之中我们反复用到了代入替换. 
而代入原理可以完全包装在谓词的结构之中. 



#definition[谓词 (predicate)][
  #term[谓词]是部分待定的语句. 
  定义谓词时, 取个名字, 设一组#term[参数], 
  写下一个含有参数的语句或表达式.
  谓词和表达式之间用定义号 $:=$ 连接. 
  可以设不止一个参数, 
  语句中每个参数也可以出现不止一次. 

  使用谓词时, 向谓词#term[代入]一组实际值, 
  即得谓词在实际值处的@命题. 
  把定义式中出现的每个参数都替换为相应实际值, 
  就是这个命题的写法.
  同一个参数出现的各处都替换为同一个值,
  不同参数也可以替换为相同的值, 即重复的实际值.
]
// 代入实际值后就能自动生成命题吗? 并不是. 
// 使谓词能得到命题的代入值组成谓词的论域. 
// 这个在论域公理那节再仔细讲解.

#example[][
  设关于命题的@谓词 $ p(a,b) := (a -> b) $
  向其中分别代入 $a = top$, $b = top$ 得到@命题 
  $ p(top, top) = (top -> top) $
  根据@真\的重言式定义, 这个命题成立. 

  同理, $p(bot, bot)$ 成立.
]

谓词有不止一种写法. 
可以把谓词名写在最前面, 
这个叫做#term[前缀表达]或#term[波兰式], 
它比较符合函数的主客关系和认知规律; 
可以把谓词名写在最后面, 
这个叫做#term[后缀表达]或#term[逆波兰式],
它比较符合自然语言前置定语的语序;
也可以用一组符号把参数分开, 
这个叫做#term[中缀表达]或#term[代数式].
只有代数式有明确运算顺序的麻烦. 

#exercise[][蕴含与否定关于真假的命题][
+ $ not bot $
// + $ top -> top $
// + $ bot -> bot $
+ $ p -> top $
+ $ bot -> top $
+ $ bot -> p $
其中 $p$ 是任何命题.
]

// 数学语言是严肃的语言. 
// 写进正文里的每句话都应当是真的, 而不总要强调 "为真"
// 或者 "成立" 云云. 
// 反之, 一个命题为真时, 才可以把这个命题写进正文. 

非真即假是定义层面的事实. 
现在 $T_(3 (1))$ 指出非假即真, 
补全这个真假互斥的闭环, 
保证了命题常量确实只有截然不同的两个: 
真命题 (它成立), 假命题 (它不成立). 

$T_(3 (4))$ 是一个著名的愚人节玩笑: 
Matrix67 开发了一个万能程序, 
无论用户输入任何命题, 
这个程序都可以给出他的一个充分条件.
但这个程序只是在输入的字符串前面加上
"$|x|<0==>$" 而已. 它的证明可以直接从
$T_(3 (2))$ 做逆否引入, 也可以从
$T_(3 (3))$ 和平凡的 $bot -> bot$ 做两难推理.

$T_(3 (3))$ 看起来非常不可思议, 
但这确实是前提引入公理所允许的.
假蕴含真, 不意味着假就是真, 
因为真不蕴含假, 这是我们接下来讨论的内容.

否定和其他的运算可以合写. 对蕴含式的否定, 
可以把否定符号写成划在蕴含箭头上的斜杠, 
来合成谓词 #term[不蕴含] $arrow.not$, 即
$ p arrow.not q := not (p -> q) $

#theorem[蕴含不是恒真的谓词][$
  top arrow.not bot 
$]
推理形式只面向命题成立的一半, 
因此面对不成立的那一半命题, 
需采用归谬法使得推理能够进行.
// 归谬法的原理还没法说明

#proof[真不蕴含假][

  假设 $top -> bot$ 成立, 由假言推理, 
  前件 $top$ 成立, 导致后件 $bot$ 成立. 
  但 $bot$ 不成立, 矛盾!  

  因此 $top -> bot$ 不成立, 即为所证.
  #h(1fr) $qed$
]

// 先不急着列真值表, 这个放在量词前面和合取择取一起列

== 合取与择取

前面明确了蕴含与否定的内涵, 
但不蕴含仍难以处理. 
下面引入的择取虽然只是蕴含式的简单换皮, 
但能给出更加对称的性质和更显而易见的推理规则. 

#definition[择取 (disjunction)][
  #term[择取]是描述两个@命题\的非此即彼关系的@谓词,
  通常说成 
  "#term[前项]或者#term[后项]". 
  $ P_a or P_c := not P_a -> P_c $
  #divide()
  @择取\可以与@否定\合写成#term[Peirce箭头], 即
  $ p arrow.b q := not (p or q) $
]

传统的教材中将这一概念称为 "析取", 
但这明显来自相应西文概念的误译, 
"析" 字本身描绘的图景应当是异或.
// 值得一提的是, 类似于 "不是...则是..." 的关联词, 
// 一方面可以按字面解读成蕴含和否定的联合, 
// 另一方面可以按关联词的整体使用习惯解读成择取. 

择取的运算优先级比蕴含高, 比否定低. 
"不择取" 的优先级和择取相同, 
它的符号是把否定符号划在择取符号上
"$\/ #h(-0.5em) or $", 再演变而成的向下箭头 $arrow.b$.

#exercise[][择取的简单算律][
// 真不蕴含假
+ $ bot arrow.b bot $
// 支配律, 源自空证明或平凡证明
+ $ top or a $
// 源自前提引入
+ $ a -> b or a $
// 交换律, 源自否定引入
+ $ a or b -> b or a $
// // 蕴含分配
// + $ a or (b or c) -> (a or b) or (a or c) $
// 排中律, 源自重言式或双重否定消除
+ $ (not a) or a $
// 特征律
+ $ bot or a -> a $
// 幂等律
+ $ a or a -> a $
// 取逆元
+ $ a arrow.b b -> not a $
]

// 以下推理形式较完整地表达了择取式的引入和消除.

#algorithm[附加式 (addition)][$
  p / (quad p or q quad) 
$]<附加式>
#proof[][
  由附加律 $T_(4 (2))$ 和交换律 $T_(4 (4))$ 
  做假言三段论 (@假言三段论) 得 $p -> p or q$, 
  再由 $p$ 做假言推理 (@假言推理) 得 $p or q$.
  #h(1fr) $qed$
]

将蕴含包装成择取本身意义有限, 
特别是它还没有包括新的思想. 
为此我们逐渐引入合取的概念.
// 我们在@假言推理 那里就用到了两条命题同时成立这种结构. 
// 合取这个谓词就是用来表示是否处于这种状态. 
// 用语需修缮
// 为此我们先介绍一些简单的推理形式, 
// 来让合取的定义呼之欲出.

// #algorithm[约简式 (simplification)][$
//   (quad p and q quad) / p
// $]

#algorithm[合取式 (conjunction)][$
  (p \ q)/(quad p and q quad)
$]

合取式的精髓在于它把两条语句合并到一条语句之中. 
这就是我们索求的新的思想. 
为此我们可以来回顾前面的推理形式, 
它们其实已经用到了多个命题同时成立的判断, 
只不过这些命题只是散漫地陈列着, 并不能真正的联合.
// 比如因为前面没用到而实在是不想写的取拒式. 

#algorithm[拒取式 (modus tollens)][$
  (quad p->q quad\ not q)/(not p) 
$]<拒取式>
#proof[拒取式][
  根据否定引入 (@否定引入), 由 $p->q$
  做假言推理 (@假言推理) 得 $not q -> not p$, 
  再由 $not q$ 做假言推理得 $not p$. 
  #h(1fr) $qed$
]
拒取式和假言推理 (@假言推理) 对照, 
可以看出是把两个条件之一与结论对换, 
从而获得否定性的表达式的. 
这种对换可以视为一种可以对算法进行编制修订的元算法. 
// 其实在这些推理形式中的每条语句地位相等 (后面会知道), 
我们还可以拿出假言推理式中的蕴含式来和结论对换. 
这样我们就得到了苦之久矣的对蕴含式的否定方法, 
否定后件, 肯定前件, 即
#corollary[拒取式II][$
  (not &q \ &p)/(quad not (p -> q) quad)
$]

比对合取式, 也许你发现了什么. 
是的, 虽然这根本不是可以证明的, 
但是结构的如此接近使得合取的定义呼之欲出: 

#definition[合取 (conjunction)][
  #term[合取]是描述两个命题的同时成立关系的谓词, 
  通常说成 "@前项\并且@后项". 
  $ P_a and P_c := not (P_a -> not P_c) $
  #divide()
  @合取\可以与@否定\合写成#term[Sheffer竖线], 即
  $ p arrow.t q := not (p and q) $
]

合取的运算优先级比否定低, 习惯上高于择取. 
"不合取" 的优先级和合取相同, 
它的符号是把否定符号划在合取符号上
"$\/ #h(-0.6em) and $", 再演变而成的向上箭头 $arrow.t$.

#exercise[][合取的简单算律][
+ $ top and top $
+ $ bot arrow.t a $
+ $ a and b -> a $
+ $ a and b -> b and a $
+ $ a arrow.t not a $
+ $ a -> a and top $
+ $ a -> a and a $
+ $ not a -> a arrow.t b $
]

#figure(
  caption: "二元命题谓词的真值表", 

  placement: auto
)[
  #table(
    columns: 6,
    row-gutter: (auto, 2.2pt, auto),
    table.header(
      [左元], $p$, $bot$, $bot$, $top$, $top$, 
      [右元], $q$, $bot$, $top$, $bot$, $top$, 
      table.hline(stroke: rgb("c9c")), 
    ),
    [@假], $bot$, $bot$, $bot$, $bot$, $bot$,
    [@合取], $p and q$, $bot$, $bot$, $bot$, $top$, 
    [@不蕴含], $p arrow.r.not q$, $bot$, $bot$, $top$, $bot$, 
    [取左元], $p$, $bot$, $bot$, $top$, $top$, 
    [@不蕴含于], $p arrow.l.not q$, $bot$, $top$, $bot$, $bot$, 
    [取右元], $q$, $bot$, $top$, $bot$, $top$, 
    [@异或], $p xor q$, $bot$, $top$, $top$, $bot$,
    [@择取], $p or q$, $bot$, $top$, $top$, $top$,
    [不择取], $p arrow.b q$, $top$, $bot$, $bot$, $bot$,
    [@等价], $p arrow.l.r q$, $top$, $bot$, $bot$, $top$, 
    [非右元], $not q$, $top$, $bot$, $top$, $bot$,
    [@蕴含于], $p arrow.l q$, $top$, $bot$, $top$, $top$, 
    [非左元], $not p$, $top$, $top$, $bot$, $bot$,
    [@蕴含], $p arrow q$, $top$, $top$, $bot$, $top$,
    [不合取], $p arrow.t q$, $top$, $top$, $top$, $bot$,
    [@真], $top$, $top$, $top$, $top$, $top$,
  )
]<二元命题谓词>

仅考虑真值的二元命题谓词,
当两个命题分别选取真假时, 
这些谓词的真假列如@二元命题谓词 所示. 
本质上只有16个不同的二元命题谓词. 
这其中的一些表达式看起来并不同时包含 $p$ 和 $q$, 
// 但这样的表达式仍然可以是二元谓词, 
只不过是它关于那个未出现的字母是常谓词.

#definition[其他二元命题谓词][
  #place[
    / #term[蕴含于] :
    / #term[不蕴含于] :
  ]
  $ 
    a <- b &:= b -> a \
    a arrow.l.not b &:= not (b -> a) 
  $
  #place[
    / #term[等价] :
    / #term[异或] :
  ]
  $ 
    a <-> b &:= (a -> b) and (b -> a) \
    a xor b &:= (a or b) and not (a and b)
  $
]

合取与择取存在某种深刻的对称联系. 

#theorem[de Morgan 律][$
  not (p and q) <--> (not p) or (not q) \
  not (p or q) <--> (not p) and (not q)
$]
#proof[][
  比对@合取\和@择取\的定义, 可以看到
  $ 
    not (p and q) &= not (not (p -> not q)) \
    &<--> not (not p) -> not q \
    &= not p or not q
  $
  代入 $p = not a$, $q = not b$, 即
  $ 
    not(not a and not b) 
    <--> not (not a) or not (not b) 
  $
  做逆否引入 (@否定引入) 和双重否定消除 (@否定消除), 即得
  $ 
    not (a or b) <--> not a and not b
  $
  #h(1fr) $qed$
]
证明过程中使用了等号和双箭头. 
本文对此做出区分: 仅代入定义式的使用等号,
而应用逻辑规律的等价变形则使用双箭头.

我们称只用且或非连结诸变量的逻辑表达式为#term[布尔表达式], 称 $({top, bot}, not, and, or)$ 是一个#term[布尔代数]. 
进一步地, 对于布尔表达式, 将其中的每一个 $or$ 和 $and$ 对调, $top$ 和 $bot$ 对调, 则得到它的对偶式; 在对偶式的基础上再否定每个变量, 则得到它的反演式. 

#exercise[][请证明布尔表达式和它的反演式等价.]

// #lorem(1200)

#algorithm[选言三段论\ (Disjunctive syllogism)][$
  (quad p or q quad \ not p) / q 
$]
#proof[][
  由择取的定义将 $p or q$ 改写成 $not p -> q$, 
  再由 $not p$ 做假言推理得 $q$. 
  #h(1fr) $qed$
]
// $T_(4,6)$ 的证明比它困难.
#algorithm[消解式 (resolution)][$ 
  (quad p & or q quad \ not p & or r)/(q or r) 
$]
#proof[][
  由择取的定义将 $p or q$ 改写成 $not p -> q$, 
  将 $not p or r$ 改写成 $not (not p) -> r$. 
  向附加律 $T_(4,2)$ 中轮换代入 $q$ 和 $r$ 得到
  $q -> r or q$ 和 $r -> q or r$. 
  再考虑交换律 $T_(4,4)$ 和双重否定引入(@双重否定引入)), 陈列为: 
  $
    p &-> not (not p) \
    not (not p) &-> r \
    r &-> q or r \
    not p &-> q \
    q &-> r or q \
    r or q &-> q or r
  $
  做蕴含三段论得
  $p -> q or r$ 和 $not p -> q or r$, 
  做两难推理得 $q or r$. 
]

量词是数理逻辑的重要组成, 但量词的使用严重依赖论域.
为此先介绍集合理论. 

// 前面虽然介绍了支配律, 交换律, 特征律, 幂等律等, 
// 但并没有介绍结合律, 因为结合律的蕴含版本很丑陋. 
// 漂亮的写法是分配形式, 那么析取的结合律并不显然. 

// #theorem[析取的结合律][
//   $ a or (b or c) -> (a or b) or c $
// ]
// #proof[
//   由前提分配 (@前提分配) 
//   $ (r -> (q->p)) -> ((r -> q) -> (r -> p)) $ 
//   代入 $s = not p$ 考虑析取的定义得析取对析取的分配律
//   $ a or (b or c) -> (a or b) or (a or c) $
//   出现了 $a or b$, 但这显然不够简洁. 进一步分配, 把右边变形成
//   $ ((a or b) or a) or ((a or b) or c) $
//   再用两次吸收律, 依次得到
//   $ (a or b) or ((a or b) or c) $

//   #h(1fr)$(a or b) or c$#h(1fr)$qed$
// ]